Left Termination proof of /tmp/tmpA7d1Jt/der.pl

Left Termination of the query pattern
der(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇒, 187 ms)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇒, 524 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 103 ms)

        ↳11 QDP

        ↳12 QDPOrderProof (⇔, 529 ms)

        ↳13 QDP

        ↳14 DependencyGraphProof (⇔, 0 ms)

        ↳15 TRUE

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

(0) Obligation:

Clauses:

der(d(e(t)), const(1)).
der(d(e(const(A))), const(0)).
der(d(e(+(X, Y))), +(DX, DY)) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY)).
der(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY)).
der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX)).

Query: der(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: der(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: der(T1, T2), SCOPE: 1, CLAUSE: 0 | der(T1, T2), SCOPE: 1, CLAUSE: 1 | der(T1, T2), SCOPE: 1, CLAUSE: 2 | der(T1, T2), SCOPE: 1, CLAUSE: 3 | der(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 1 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 2 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: der(T1, T2), SCOPE: 1, CLAUSE: 1 | der(T1, T2), SCOPE: 1, CLAUSE: 2 | der(T1, T2), SCOPE: 1, CLAUSE: 3 | der(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nder(T1, T2) !=? der(d(e(t)), const(1))", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: der(d(e(t)), T2), SCOPE: 1, CLAUSE: 1 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 2 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: der(d(e(t)), T2), SCOPE: 1, CLAUSE: 2 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: der(d(e(t)), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: der(d(e(t)), T2), SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 2 | der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: der(T1, T2), SCOPE: 1, CLAUSE: 2 | der(T1, T2), SCOPE: 1, CLAUSE: 3 | der(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nX13 is free\nder(T1, T2) !=? der(d(e(t)), const(1))\nder(T1, T2) !=? der(d(e(const(X13))), const(0))", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 2 | der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: der(d(e(const(T4))), T2), SCOPE: 1, CLAUSE: 4\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)) | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: der(T1, T2), SCOPE: 1, CLAUSE: 3 | der(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nX13 is free\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nder(T1, T2) !=? der(d(e(t)), const(1))\nder(T1, T2) !=? der(d(e(const(X13))), const(0))\nder(T1, T2) !=? der(d(e(+(X28, X29))), +(X30, X31))", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 0 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 1 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 0\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 1 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: der(d(e(T10)), T15)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 1\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: der(d(e(T10)), T21)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3 | ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="B: ','(','(der(d(e(T38)), T42), der(d(e(T39)), T43)), der(d(e(T10)), T44))\n\nT10 is ground\nT38 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: der(d(e(T38)), T42)\n\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(der(d(e(T39)), T45), der(d(e(T10)), T46))\n\nT10 is ground\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: der(d(e(T39)), T45)\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: der(d(e(T10)), T47)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 3\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(der(d(e(T9)), T13), der(d(e(T10)), T14)), SCOPE: 2, CLAUSE: 4 | ?_2 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(der(d(e(T64)), T68), der(d(e(T65)), T69)), der(d(e(T10)), T70))\n\nT10 is ground\nT64 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_2 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 3 | der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: der(d(e(+(T9, T10))), T2), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)) | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: der(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nX13 is free\nX28 is free\nX29 is free\nX30 is free\nX31 is free\nX89 is free\nX90 is free\nX91 is free\nX92 is free\nder(T1, T2) !=? der(d(e(t)), const(1))\nder(T1, T2) !=? der(d(e(const(X13))), const(0))\nder(T1, T2) !=? der(d(e(+(X28, X29))), +(X30, X31))\nder(T1, T2) !=? der(d(e(*(X89, X90))), +(*(X89, X91), *(X90, X92)))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 0 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 1 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 0\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 1 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: der(d(e(T76)), T81)\n\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 1\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: der(d(e(T76)), T87)\n\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 2\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3 | ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(','(der(d(e(T104)), T108), der(d(e(T105)), T109)), der(d(e(T76)), T110))\n\nT76 is ground\nT104 is ground\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 3\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(der(d(e(T75)), T79), der(d(e(T76)), T80)), SCOPE: 3, CLAUSE: 4 | ?_3 | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(','(der(d(e(T127)), T131), der(d(e(T128)), T132)), der(d(e(T76)), T133))\n\nT76 is ground\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_3 | der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: der(d(e(*(T75, T76))), T2), SCOPE: 1, CLAUSE: 4\n\nT75 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="C: ','(der(d(T136), X146), der(d(e(X146)), T138))\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 0 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 1 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 2 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 3 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 0\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 1 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 2 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 3 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: der(d(e(const(1))), T138)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 1\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 2 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 3 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: der(d(e(const(0))), T138)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 2\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 3 | ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(','(der(d(e(T152)), X180), der(d(e(T153)), X181)), der(d(e(+(X180, X181))), T138))\n\nT152 is ground\nT153 is ground\nX180 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: der(d(e(T152)), X180)\n\nT152 is ground\nX180 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(der(d(e(T153)), X181), der(d(e(+(T154, X181))), T138))\n\nT153 is ground\nT154 is ground\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: der(d(e(T153)), X181)\n\nT153 is ground\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: der(d(e(+(T154, T155))), T138)\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 3\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(der(d(T136), X146), der(d(e(X146)), T138)), SCOPE: 4, CLAUSE: 4\n\nT136 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(','(der(d(e(T164)), X211), der(d(e(T165)), X210)), der(d(e(+(*(T164, X210), *(T165, X211)))), T138))\n\nT164 is ground\nT165 is ground\nX210 is free\nX211 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: der(d(e(T164)), X211)\n\nT164 is ground\nX211 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(der(d(e(T165)), X210), der(d(e(+(*(T164, X210), *(T165, T166)))), T138))\n\nT164 is ground\nT165 is ground\nT166 is ground\nX210 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: der(d(e(T165)), X210)\n\nT165 is ground\nX210 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: der(d(e(+(*(T164, T167), *(T165, T166)))), T138)\n\nT164 is ground\nT165 is ground\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(','(der(d(T170), X221), der(d(e(X221)), X222)), der(d(e(X222)), T138))\n\nT170 is ground\nX222 is free\nX221 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: der(d(T170), X221)\n\nT170 is ground\nX221 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(der(d(e(T171)), X222), der(d(e(X222)), T138))\n\nT171 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 96 [arrowhead = none ];
96 -> 2;

97 [label="EVAL with clause\nder(d(e(t)), const(1)).\nand substitutionT1 -> d(e(t)),\nT2 -> const(1)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 97 [arrowhead = none ];
97 -> 3;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 98 [arrowhead = none ];
98 -> 4;

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 99 [arrowhead = none ];
99 -> 5;

100 [label="EVAL with clause\nder(d(e(const(X13))), const(0)).\nand substitutionX13 -> T4,\nT1 -> d(e(const(T4))),\nT2 -> const(0)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 100 [arrowhead = none ];
100 -> 10;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 101 [arrowhead = none ];
101 -> 11;

102 [label="BACKTRACK\nfor clause: der(d(e(const(A))), const(0))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 102 [arrowhead = none ];
102 -> 6;

103 [label="BACKTRACK\nfor clause: der(d(e(+(X, Y))), +(DX, DY)) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 103 [arrowhead = none ];
103 -> 7;

104 [label="BACKTRACK\nfor clause: der(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 104 [arrowhead = none ];
104 -> 8;

105 [label="BACKTRACK\nfor clause: der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 105 [arrowhead = none ];
105 -> 9;

106 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 106 [arrowhead = none ];
106 -> 12;

107 [label="EVAL with clause\nder(d(e(+(X28, X29))), +(X30, X31)) :- ','(der(d(e(X28)), X30), der(d(e(X29)), X31)).\nand substitutionX28 -> T9,\nX29 -> T10,\nT1 -> d(e(+(T9, T10))),\nX30 -> T13,\nX31 -> T14,\nT2 -> +(T13, T14),\nT11 -> T13,\nT12 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 107 [arrowhead = none ];
107 -> 16;

108 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 108 [arrowhead = none ];
108 -> 17;

109 [label="BACKTRACK\nfor clause: der(d(e(+(X, Y))), +(DX, DY)) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 109 [arrowhead = none ];
109 -> 13;

110 [label="BACKTRACK\nfor clause: der(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 110 [arrowhead = none ];
110 -> 14;

111 [label="BACKTRACK\nfor clause: der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 111 [arrowhead = none ];
111 -> 15;

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 112 [arrowhead = none ];
112 -> 18;

113 [label="EVAL with clause\nder(d(e(*(X89, X90))), +(*(X89, X91), *(X90, X92))) :- ','(der(d(e(X89)), X92), der(d(e(X90)), X91)).\nand substitutionX89 -> T75,\nX90 -> T76,\nT1 -> d(e(*(T75, T76))),\nX91 -> T80,\nX92 -> T79,\nT2 -> +(*(T75, T80), *(T76, T79)),\nT78 -> T79,\nT77 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 113 [arrowhead = none ];
113 -> 43;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 114 [arrowhead = none ];
114 -> 44;

115 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 115 [arrowhead = none ];
115 -> 19;

116 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 116 [arrowhead = none ];
116 -> 20;

117 [label="EVAL with clause\nder(d(e(t)), const(1)).\nand substitutionT9 -> t,\nT13 -> const(1),\nT14 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 117 [arrowhead = none ];
117 -> 21;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 118 [arrowhead = none ];
118 -> 22;

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 119 [arrowhead = none ];
119 -> 23;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 120 [arrowhead = none ];
120 -> 24;

121 [label="INSTANCE with matching:\nT1 -> d(e(T10))\nT2 -> T15", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 121 [arrowhead = none , style=dashed];
121 -> 1[style=dashed];

122 [label="EVAL with clause\nder(d(e(const(X36))), const(0)).\nand substitutionX36 -> T20,\nT9 -> const(T20),\nT13 -> const(0),\nT14 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 122 [arrowhead = none ];
122 -> 25;

123 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 123 [arrowhead = none ];
123 -> 26;

124 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 124 [arrowhead = none ];
124 -> 27;

125 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 125 [arrowhead = none ];
125 -> 28;

126 [label="INSTANCE with matching:\nT1 -> d(e(T10))\nT2 -> T21", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 126 [arrowhead = none , style=dashed];
126 -> 1[style=dashed];

127 [label="EVAL with clause\nder(d(e(+(X53, X54))), +(X55, X56)) :- ','(der(d(e(X53)), X55), der(d(e(X54)), X56)).\nand substitutionX53 -> T38,\nX54 -> T39,\nT9 -> +(T38, T39),\nX55 -> T42,\nX56 -> T43,\nT13 -> +(T42, T43),\nT40 -> T42,\nT41 -> T43,\nT14 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 127 [arrowhead = none ];
127 -> 29;

128 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 128 [arrowhead = none ];
128 -> 30;

129 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
28 -> 129 [arrowhead = none ];
129 -> 35;

130 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
28 -> 130 [arrowhead = none ];
130 -> 36;

131 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
29 -> 131 [arrowhead = none ];
131 -> 31;

132 [label="SPLIT 2\nnew knowledge:\nT38 is ground\nT42 is ground\nreplacements:T43 -> T45,\nT44 -> T46", fontsize=14, style = filled, fillcolor = violet];
29 -> 132 [arrowhead = none ];
132 -> 32;

133 [label="INSTANCE with matching:\nT1 -> d(e(T38))\nT2 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
31 -> 133 [arrowhead = none , style=dashed];
133 -> 1[style=dashed];

134 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
32 -> 134 [arrowhead = none ];
134 -> 33;

135 [label="SPLIT 2\nnew knowledge:\nT39 is ground\nT45 is ground\nreplacements:T46 -> T47", fontsize=14, style = filled, fillcolor = violet];
32 -> 135 [arrowhead = none ];
135 -> 34;

136 [label="INSTANCE with matching:\nT1 -> d(e(T39))\nT2 -> T45", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 136 [arrowhead = none , style=dashed];
136 -> 1[style=dashed];

137 [label="INSTANCE with matching:\nT1 -> d(e(T10))\nT2 -> T47", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 137 [arrowhead = none , style=dashed];
137 -> 1[style=dashed];

138 [label="EVAL with clause\nder(d(e(*(X73, X74))), +(*(X73, X75), *(X74, X76))) :- ','(der(d(e(X73)), X76), der(d(e(X74)), X75)).\nand substitutionX73 -> T64,\nX74 -> T65,\nT9 -> *(T64, T65),\nX75 -> T69,\nX76 -> T68,\nT13 -> +(*(T64, T69), *(T65, T68)),\nT67 -> T68,\nT66 -> T69,\nT14 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 138 [arrowhead = none ];
138 -> 37;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 139 [arrowhead = none ];
139 -> 38;

140 [label="BACKTRACK\nfor clause: der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 140 [arrowhead = none ];
140 -> 39;

141 [label="INSTANCE with matching:\nT38 -> T64\nT42 -> T68\nT39 -> T65\nT43 -> T69\nT44 -> T70", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 141 [arrowhead = none , style=dashed];
141 -> 29[style=dashed];

142 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 142 [arrowhead = none ];
142 -> 40;

143 [label="BACKTRACK\nfor clause: der(d(e(*(X, Y))), +(*(X, DY), *(Y, DX))) :- ','(der(d(e(X)), DX), der(d(e(Y)), DY))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 143 [arrowhead = none ];
143 -> 41;

144 [label="BACKTRACK\nfor clause: der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 144 [arrowhead = none ];
144 -> 42;

145 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 145 [arrowhead = none ];
145 -> 45;

146 [label="EVAL with clause\nder(d(d(X144)), X145) :- ','(der(d(X144), X146), der(d(e(X146)), X145)).\nand substitutionX144 -> T136,\nT1 -> d(d(T136)),\nT2 -> T138,\nX145 -> T138,\nT137 -> T138", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 146 [arrowhead = none ];
146 -> 65;

147 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 147 [arrowhead = none ];
147 -> 66;

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 148 [arrowhead = none ];
148 -> 46;

149 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 149 [arrowhead = none ];
149 -> 47;

150 [label="EVAL with clause\nder(d(e(t)), const(1)).\nand substitutionT75 -> t,\nT79 -> const(1),\nT80 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 150 [arrowhead = none ];
150 -> 48;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 151 [arrowhead = none ];
151 -> 49;

152 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
47 -> 152 [arrowhead = none ];
152 -> 50;

153 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
47 -> 153 [arrowhead = none ];
153 -> 51;

154 [label="INSTANCE with matching:\nT1 -> d(e(T76))\nT2 -> T81", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 154 [arrowhead = none , style=dashed];
154 -> 1[style=dashed];

155 [label="EVAL with clause\nder(d(e(const(X97))), const(0)).\nand substitutionX97 -> T86,\nT75 -> const(T86),\nT79 -> const(0),\nT80 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 155 [arrowhead = none ];
155 -> 52;

156 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 156 [arrowhead = none ];
156 -> 53;

157 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 157 [arrowhead = none ];
157 -> 54;

158 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
51 -> 158 [arrowhead = none ];
158 -> 55;

159 [label="INSTANCE with matching:\nT1 -> d(e(T76))\nT2 -> T87", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 159 [arrowhead = none , style=dashed];
159 -> 1[style=dashed];

160 [label="EVAL with clause\nder(d(e(+(X114, X115))), +(X116, X117)) :- ','(der(d(e(X114)), X116), der(d(e(X115)), X117)).\nand substitutionX114 -> T104,\nX115 -> T105,\nT75 -> +(T104, T105),\nX116 -> T108,\nX117 -> T109,\nT79 -> +(T108, T109),\nT106 -> T108,\nT107 -> T109,\nT80 -> T110", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 160 [arrowhead = none ];
160 -> 56;

161 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 161 [arrowhead = none ];
161 -> 57;

162 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 162 [arrowhead = none ];
162 -> 58;

163 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
55 -> 163 [arrowhead = none ];
163 -> 59;

164 [label="INSTANCE with matching:\nT38 -> T104\nT42 -> T108\nT39 -> T105\nT43 -> T109\nT10 -> T76\nT44 -> T110", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 164 [arrowhead = none , style=dashed];
164 -> 29[style=dashed];

165 [label="EVAL with clause\nder(d(e(*(X134, X135))), +(*(X134, X136), *(X135, X137))) :- ','(der(d(e(X134)), X137), der(d(e(X135)), X136)).\nand substitutionX134 -> T127,\nX135 -> T128,\nT75 -> *(T127, T128),\nX136 -> T132,\nX137 -> T131,\nT79 -> +(*(T127, T132), *(T128, T131)),\nT130 -> T131,\nT129 -> T132,\nT80 -> T133", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 165 [arrowhead = none ];
165 -> 60;

166 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 166 [arrowhead = none ];
166 -> 61;

167 [label="BACKTRACK\nfor clause: der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 167 [arrowhead = none ];
167 -> 62;

168 [label="INSTANCE with matching:\nT38 -> T127\nT42 -> T131\nT39 -> T128\nT43 -> T132\nT10 -> T76\nT44 -> T133", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 168 [arrowhead = none , style=dashed];
168 -> 29[style=dashed];

169 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 169 [arrowhead = none ];
169 -> 63;

170 [label="BACKTRACK\nfor clause: der(d(d(X)), DDX) :- ','(der(d(X), DX), der(d(e(DX)), DDX))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 170 [arrowhead = none ];
170 -> 64;

171 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
65 -> 171 [arrowhead = none ];
171 -> 67;

172 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 172 [arrowhead = none ];
172 -> 68;

173 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 173 [arrowhead = none ];
173 -> 69;

174 [label="EVAL with clause\nder(d(e(t)), const(1)).\nand substitutionT136 -> e(t),\nX146 -> const(1)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 174 [arrowhead = none ];
174 -> 70;

175 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 175 [arrowhead = none ];
175 -> 71;

176 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
69 -> 176 [arrowhead = none ];
176 -> 72;

177 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
69 -> 177 [arrowhead = none ];
177 -> 73;

178 [label="INSTANCE with matching:\nT1 -> d(e(const(1)))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 178 [arrowhead = none , style=dashed];
178 -> 1[style=dashed];

179 [label="EVAL with clause\nder(d(e(const(X151))), const(0)).\nand substitutionX151 -> T143,\nT136 -> e(const(T143)),\nX146 -> const(0)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 179 [arrowhead = none ];
179 -> 74;

180 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 180 [arrowhead = none ];
180 -> 75;

181 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 181 [arrowhead = none ];
181 -> 76;

182 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 182 [arrowhead = none ];
182 -> 77;

183 [label="INSTANCE with matching:\nT1 -> d(e(const(0)))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 183 [arrowhead = none , style=dashed];
183 -> 1[style=dashed];

184 [label="EVAL with clause\nder(d(e(+(X176, X177))), +(X178, X179)) :- ','(der(d(e(X176)), X178), der(d(e(X177)), X179)).\nand substitutionX176 -> T152,\nX177 -> T153,\nT136 -> e(+(T152, T153)),\nX178 -> X180,\nX179 -> X181,\nX146 -> +(X180, X181)", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 184 [arrowhead = none ];
184 -> 78;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 185 [arrowhead = none ];
185 -> 79;

186 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 186 [arrowhead = none ];
186 -> 84;

187 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
77 -> 187 [arrowhead = none ];
187 -> 85;

188 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
78 -> 188 [arrowhead = none ];
188 -> 80;

189 [label="SPLIT 2\nnew knowledge:\nT152 is ground\nT154 is ground\nreplacements:X180 -> T154", fontsize=14, style = filled, fillcolor = violet];
78 -> 189 [arrowhead = none ];
189 -> 81;

190 [label="INSTANCE with matching:\nT1 -> d(e(T152))\nT2 -> X180", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 190 [arrowhead = none , style=dashed];
190 -> 1[style=dashed];

191 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
81 -> 191 [arrowhead = none ];
191 -> 82;

192 [label="SPLIT 2\nnew knowledge:\nT153 is ground\nT155 is ground\nreplacements:X181 -> T155", fontsize=14, style = filled, fillcolor = violet];
81 -> 192 [arrowhead = none ];
192 -> 83;

193 [label="INSTANCE with matching:\nT1 -> d(e(T153))\nT2 -> X181", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 193 [arrowhead = none , style=dashed];
193 -> 1[style=dashed];

194 [label="INSTANCE with matching:\nT1 -> d(e(+(T154, T155)))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
83 -> 194 [arrowhead = none , style=dashed];
194 -> 1[style=dashed];

195 [label="EVAL with clause\nder(d(e(*(X206, X207))), +(*(X206, X208), *(X207, X209))) :- ','(der(d(e(X206)), X209), der(d(e(X207)), X208)).\nand substitutionX206 -> T164,\nX207 -> T165,\nT136 -> e(*(T164, T165)),\nX208 -> X210,\nX209 -> X211,\nX146 -> +(*(T164, X210), *(T165, X211))", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 195 [arrowhead = none ];
195 -> 86;

196 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 196 [arrowhead = none ];
196 -> 87;

197 [label="EVAL with clause\nder(d(d(X219)), X220) :- ','(der(d(X219), X221), der(d(e(X221)), X220)).\nand substitutionX219 -> T170,\nT136 -> d(T170),\nX146 -> X222,\nX220 -> X222", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 197 [arrowhead = none ];
197 -> 92;

198 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 198 [arrowhead = none ];
198 -> 93;

199 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
86 -> 199 [arrowhead = none ];
199 -> 88;

200 [label="SPLIT 2\nnew knowledge:\nT164 is ground\nT166 is ground\nreplacements:X211 -> T166", fontsize=14, style = filled, fillcolor = violet];
86 -> 200 [arrowhead = none ];
200 -> 89;

201 [label="INSTANCE with matching:\nT1 -> d(e(T164))\nT2 -> X211", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 201 [arrowhead = none , style=dashed];
201 -> 1[style=dashed];

202 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
89 -> 202 [arrowhead = none ];
202 -> 90;

203 [label="SPLIT 2\nnew knowledge:\nT165 is ground\nT167 is ground\nreplacements:X210 -> T167", fontsize=14, style = filled, fillcolor = violet];
89 -> 203 [arrowhead = none ];
203 -> 91;

204 [label="INSTANCE with matching:\nT1 -> d(e(T165))\nT2 -> X210", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 204 [arrowhead = none , style=dashed];
204 -> 1[style=dashed];

205 [label="INSTANCE with matching:\nT1 -> d(e(+(*(T164, T167), *(T165, T166))))\nT2 -> T138", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 205 [arrowhead = none , style=dashed];
205 -> 1[style=dashed];

206 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
92 -> 206 [arrowhead = none ];
206 -> 94;

207 [label="SPLIT 2\nnew knowledge:\nT170 is ground\nT171 is ground\nreplacements:X221 -> T171", fontsize=14, style = filled, fillcolor = violet];
92 -> 207 [arrowhead = none ];
207 -> 95;

208 [label="INSTANCE with matching:\nT1 -> d(T170)\nT2 -> X221", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 208 [arrowhead = none , style=dashed];
208 -> 1[style=dashed];

209 [label="INSTANCE with matching:\nT136 -> e(T171)\nX146 -> X222", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 209 [arrowhead = none , style=dashed];
209 -> 65[style=dashed];

}

(2) Obligation:

Triples:

pB(X1, X2, X3, X4, X5, X6) :- derA(d(e(X1)), X2).
pB(X1, X2, X3, X4, X5, X6) :- ','(dercA(d(e(X1)), X2), derA(d(e(X3)), X4)).
pB(X1, X2, X3, X4, X5, X6) :- ','(dercA(d(e(X1)), X2), ','(dercA(d(e(X3)), X4), derA(d(e(X5)), X6))).
pC(e(t), const(1), X1) :- derA(d(e(const(1))), X1).
pC(e(const(X1)), const(0), X2) :- derA(d(e(const(0))), X2).
pC(e(+(X1, X2)), +(X3, X4), X5) :- derA(d(e(X1)), X3).
pC(e(+(X1, X2)), +(X3, X4), X5) :- ','(dercA(d(e(X1)), X3), derA(d(e(X2)), X4)).
pC(e(+(X1, X2)), +(X3, X4), X5) :- ','(dercA(d(e(X1)), X3), ','(dercA(d(e(X2)), X4), derA(d(e(+(X3, X4))), X5))).
pC(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) :- derA(d(e(X1)), X4).
pC(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) :- ','(dercA(d(e(X1)), X4), derA(d(e(X2)), X3)).
pC(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) :- ','(dercA(d(e(X1)), X4), ','(dercA(d(e(X2)), X3), derA(d(e(+(*(X1, X3), *(X2, X4)))), X5))).
pC(d(X1), X2, X3) :- derA(d(X1), X4).
pC(d(X1), X2, X3) :- ','(dercA(d(X1), X4), pC(e(X4), X2, X3)).
derA(d(e(+(t, X1))), +(const(1), X2)) :- derA(d(e(X1)), X2).
derA(d(e(+(const(X1), X2))), +(const(0), X3)) :- derA(d(e(X2)), X3).
derA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) :- pB(X1, X4, X2, X5, X3, X6).
derA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) :- pB(X1, X5, X2, X4, X3, X6).
derA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) :- derA(d(e(X1)), X2).
derA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) :- derA(d(e(X2)), X3).
derA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) :- pB(X1, X5, X2, X6, X3, X4).
derA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) :- pB(X1, X6, X2, X5, X3, X4).
derA(d(d(X1)), X2) :- pC(X1, X3, X2).

Clauses:

dercA(d(e(t)), const(1)).
dercA(d(e(const(X1))), const(0)).
dercA(d(e(+(t, X1))), +(const(1), X2)) :- dercA(d(e(X1)), X2).
dercA(d(e(+(const(X1), X2))), +(const(0), X3)) :- dercA(d(e(X2)), X3).
dercA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) :- qcB(X1, X4, X2, X5, X3, X6).
dercA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) :- qcB(X1, X5, X2, X4, X3, X6).
dercA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) :- dercA(d(e(X1)), X2).
dercA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) :- dercA(d(e(X2)), X3).
dercA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) :- qcB(X1, X5, X2, X6, X3, X4).
dercA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) :- qcB(X1, X6, X2, X5, X3, X4).
dercA(d(d(X1)), X2) :- qcC(X1, X3, X2).
qcB(X1, X2, X3, X4, X5, X6) :- ','(dercA(d(e(X1)), X2), ','(dercA(d(e(X3)), X4), dercA(d(e(X5)), X6))).
qcC(e(t), const(1), X1) :- dercA(d(e(const(1))), X1).
qcC(e(const(X1)), const(0), X2) :- dercA(d(e(const(0))), X2).
qcC(e(+(X1, X2)), +(X3, X4), X5) :- ','(dercA(d(e(X1)), X3), ','(dercA(d(e(X2)), X4), dercA(d(e(+(X3, X4))), X5))).
qcC(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) :- ','(dercA(d(e(X1)), X4), ','(dercA(d(e(X2)), X3), dercA(d(e(+(*(X1, X3), *(X2, X4)))), X5))).
qcC(d(X1), X2, X3) :- ','(dercA(d(X1), X4), qcC(e(X4), X2, X3)).

Afs:

derA(x1, x2) = derA(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
derA_in: (b,f)
pB_in: (b,f,b,f,b,f)
dercA_in: (b,f)
qcB_in: (b,f,b,f,b,f)
qcC_in: (b,f,f)
pC_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DERA_IN_GA(d(e(+(t, X1))), +(const(1), X2)) → U21_GA(X1, X2, derA_in_ga(d(e(X1)), X2))
DERA_IN_GA(d(e(+(t, X1))), +(const(1), X2)) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(const(X1), X2))), +(const(0), X3)) → U22_GA(X1, X2, X3, derA_in_ga(d(e(X2)), X3))
DERA_IN_GA(d(e(+(const(X1), X2))), +(const(0), X3)) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U23_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X4, X2, X5, X3, X6))
DERA_IN_GA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → PB_IN_GAGAGA(X1, X4, X2, X5, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → U1_GAGAGA(X1, X2, X3, X4, X5, X6, derA_in_ga(d(e(X1)), X2))
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U24_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X5, X2, X4, X3, X6))
DERA_IN_GA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → PB_IN_GAGAGA(X1, X5, X2, X4, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U3_GAGAGA(X1, X2, X3, X4, X5, X6, derA_in_ga(d(e(X3)), X4))
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → DERA_IN_GA(d(e(X3)), X4)
DERA_IN_GA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U25_GA(X1, X2, derA_in_ga(d(e(X1)), X2))
DERA_IN_GA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U26_GA(X1, X2, X3, derA_in_ga(d(e(X2)), X3))
DERA_IN_GA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U27_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X5, X2, X6, X3, X4))
DERA_IN_GA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → PB_IN_GAGAGA(X1, X5, X2, X6, X3, X4)
DERA_IN_GA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U28_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X6, X2, X5, X3, X4))
DERA_IN_GA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → PB_IN_GAGAGA(X1, X6, X2, X5, X3, X4)
DERA_IN_GA(d(d(X1)), X2) → U29_GA(X1, X2, pC_in_gaa(X1, X3, X2))
DERA_IN_GA(d(d(X1)), X2) → PC_IN_GAA(X1, X3, X2)
PC_IN_GAA(e(t), const(1), X1) → U6_GAA(X1, derA_in_ga(d(e(const(1))), X1))
PC_IN_GAA(e(t), const(1), X1) → DERA_IN_GA(d(e(const(1))), X1)
PC_IN_GAA(e(const(X1)), const(0), X2) → U7_GAA(X1, X2, derA_in_ga(d(e(const(0))), X2))
PC_IN_GAA(e(const(X1)), const(0), X2) → DERA_IN_GA(d(e(const(0))), X2)
PC_IN_GAA(e(+(X1, X2)), +(X3, X4), X5) → U8_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X1)), X3))
PC_IN_GAA(e(+(X1, X2)), +(X3, X4), X5) → DERA_IN_GA(d(e(X1)), X3)
PC_IN_GAA(e(+(X1, X2)), +(X3, X4), X5) → U9_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X3))
U9_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U10_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X2)), X4))
U9_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → DERA_IN_GA(d(e(X2)), X4)
U9_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U11_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X4))
U11_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → U12_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(+(X3, X4))), X5))
U11_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → DERA_IN_GA(d(e(+(X3, X4))), X5)
PC_IN_GAA(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U13_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X1)), X4))
PC_IN_GAA(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → DERA_IN_GA(d(e(X1)), X4)
PC_IN_GAA(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U14_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X4))
U14_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U15_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X2)), X3))
U14_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → DERA_IN_GA(d(e(X2)), X3)
U14_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U16_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X3))
U16_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → U17_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5))
U16_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → DERA_IN_GA(d(e(+(*(X1, X3), *(X2, X4)))), X5)
PC_IN_GAA(d(X1), X2, X3) → U18_GAA(X1, X2, X3, derA_in_ga(d(X1), X4))
PC_IN_GAA(d(X1), X2, X3) → DERA_IN_GA(d(X1), X4)
PC_IN_GAA(d(X1), X2, X3) → U19_GAA(X1, X2, X3, dercA_in_ga(d(X1), X4))
U19_GAA(X1, X2, X3, dercA_out_ga(d(X1), X4)) → U20_GAA(X1, X2, X3, pC_in_gaa(e(X4), X2, X3))
U19_GAA(X1, X2, X3, dercA_out_ga(d(X1), X4)) → PC_IN_GAA(e(X4), X2, X3)
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U5_GAGAGA(X1, X2, X3, X4, X5, X6, derA_in_ga(d(e(X5)), X6))
U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → DERA_IN_GA(d(e(X5)), X6)

The TRS R consists of the following rules:

dercA_in_ga(d(e(t)), const(1)) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1))), const(0)) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1))), +(const(1), X2)) → U31_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(const(X1), X2))), +(const(0), X3)) → U32_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U33_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X4, X2, X5, X3, X6))
qcB_in_gagaga(X1, X2, X3, X4, X5, X6) → U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U34_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X4, X3, X6))
U34_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
dercA_in_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U35_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U36_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U37_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X6, X3, X4))
U37_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
dercA_in_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U38_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X6, X2, X5, X3, X4))
U38_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
dercA_in_ga(d(d(X1)), X2) → U39_ga(X1, X2, qcC_in_gaa(X1, X3, X2))
qcC_in_gaa(e(t), const(1), X1) → U43_gaa(X1, dercA_in_ga(d(e(const(1))), X1))
U43_gaa(X1, dercA_out_ga(d(e(const(1))), X1)) → qcC_out_gaa(e(t), const(1), X1)
qcC_in_gaa(e(const(X1)), const(0), X2) → U44_gaa(X1, X2, dercA_in_ga(d(e(const(0))), X2))
U44_gaa(X1, X2, dercA_out_ga(d(e(const(0))), X2)) → qcC_out_gaa(e(const(X1)), const(0), X2)
qcC_in_gaa(e(+(X1, X2)), +(X3, X4), X5) → U45_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X3))
U45_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U46_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X4))
U46_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → U47_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(X3, X4))), X5))
U47_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(X3, X4))), X5)) → qcC_out_gaa(e(+(X1, X2)), +(X3, X4), X5)
qcC_in_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U48_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X4))
U48_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U49_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X3))
U49_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → U50_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5))
U50_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5)) → qcC_out_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5)
qcC_in_gaa(d(X1), X2, X3) → U51_gaa(X1, X2, X3, dercA_in_ga(d(X1), X4))
U51_gaa(X1, X2, X3, dercA_out_ga(d(X1), X4)) → U52_gaa(X1, X2, X3, qcC_in_gaa(e(X4), X2, X3))
U52_gaa(X1, X2, X3, qcC_out_gaa(e(X4), X2, X3)) → qcC_out_gaa(d(X1), X2, X3)
U39_ga(X1, X2, qcC_out_gaa(X1, X3, X2)) → dercA_out_ga(d(d(X1)), X2)
U36_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U35_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X5)), X6))
U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)
U33_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U32_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U31_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))

The argument filtering Pi contains the following mapping:
derA_in_ga(x1, x2) = derA_in_ga(x1)
d(x1) = d(x1)
e(x1) = e(x1)
+(x1, x2) = +(x1, x2)
t = t
const(x1) = const(x1)
pB_in_gagaga(x1, x2, x3, x4, x5, x6) = pB_in_gagaga(x1, x3, x5)
*(x1, x2) = *(x1, x2)
dercA_in_ga(x1, x2) = dercA_in_ga(x1)
dercA_out_ga(x1, x2) = dercA_out_ga(x1, x2)
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
U33_ga(x1, x2, x3, x4, x5, x6, x7) = U33_ga(x1, x2, x3, x7)
qcB_in_gagaga(x1, x2, x3, x4, x5, x6) = qcB_in_gagaga(x1, x3, x5)
U40_gagaga(x1, x2, x3, x4, x5, x6, x7) = U40_gagaga(x1, x3, x5, x7)
U34_ga(x1, x2, x3, x4, x5, x6, x7) = U34_ga(x1, x2, x3, x7)
qcB_out_gagaga(x1, x2, x3, x4, x5, x6) = qcB_out_gagaga(x1, x2, x3, x4, x5, x6)
U35_ga(x1, x2, x3) = U35_ga(x1, x3)
U36_ga(x1, x2, x3, x4) = U36_ga(x1, x2, x4)
U37_ga(x1, x2, x3, x4, x5, x6, x7) = U37_ga(x1, x2, x3, x7)
U38_ga(x1, x2, x3, x4, x5, x6, x7) = U38_ga(x1, x2, x3, x7)
U39_ga(x1, x2, x3) = U39_ga(x1, x3)
qcC_in_gaa(x1, x2, x3) = qcC_in_gaa(x1)
U43_gaa(x1, x2) = U43_gaa(x2)
1 = 1
qcC_out_gaa(x1, x2, x3) = qcC_out_gaa(x1, x2, x3)
U44_gaa(x1, x2, x3) = U44_gaa(x1, x3)
0 = 0
U45_gaa(x1, x2, x3, x4, x5, x6) = U45_gaa(x1, x2, x6)
U46_gaa(x1, x2, x3, x4, x5, x6) = U46_gaa(x1, x2, x3, x6)
U47_gaa(x1, x2, x3, x4, x5, x6) = U47_gaa(x1, x2, x3, x4, x6)
U48_gaa(x1, x2, x3, x4, x5, x6) = U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6) = U49_gaa(x1, x2, x4, x6)
U50_gaa(x1, x2, x3, x4, x5, x6) = U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4) = U51_gaa(x1, x4)
U52_gaa(x1, x2, x3, x4) = U52_gaa(x1, x4)
U41_gagaga(x1, x2, x3, x4, x5, x6, x7) = U41_gagaga(x1, x2, x3, x5, x7)
U42_gagaga(x1, x2, x3, x4, x5, x6, x7) = U42_gagaga(x1, x2, x3, x4, x5, x7)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
DERA_IN_GA(x1, x2) = DERA_IN_GA(x1)
U21_GA(x1, x2, x3) = U21_GA(x1, x3)
U22_GA(x1, x2, x3, x4) = U22_GA(x1, x2, x4)
U23_GA(x1, x2, x3, x4, x5, x6, x7) = U23_GA(x1, x2, x3, x7)
PB_IN_GAGAGA(x1, x2, x3, x4, x5, x6) = PB_IN_GAGAGA(x1, x3, x5)
U1_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U1_GAGAGA(x1, x3, x5, x7)
U24_GA(x1, x2, x3, x4, x5, x6, x7) = U24_GA(x1, x2, x3, x7)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U2_GAGAGA(x1, x3, x5, x7)
U3_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U3_GAGAGA(x1, x3, x5, x7)
U25_GA(x1, x2, x3) = U25_GA(x1, x3)
U26_GA(x1, x2, x3, x4) = U26_GA(x1, x2, x4)
U27_GA(x1, x2, x3, x4, x5, x6, x7) = U27_GA(x1, x2, x3, x7)
U28_GA(x1, x2, x3, x4, x5, x6, x7) = U28_GA(x1, x2, x3, x7)
U29_GA(x1, x2, x3) = U29_GA(x1, x3)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U6_GAA(x1, x2) = U6_GAA(x2)
U7_GAA(x1, x2, x3) = U7_GAA(x1, x3)
U8_GAA(x1, x2, x3, x4, x5, x6) = U8_GAA(x1, x2, x6)
U9_GAA(x1, x2, x3, x4, x5, x6) = U9_GAA(x1, x2, x6)
U10_GAA(x1, x2, x3, x4, x5, x6) = U10_GAA(x1, x2, x6)
U11_GAA(x1, x2, x3, x4, x5, x6) = U11_GAA(x1, x2, x3, x6)
U12_GAA(x1, x2, x3, x4, x5, x6) = U12_GAA(x1, x2, x6)
U13_GAA(x1, x2, x3, x4, x5, x6) = U13_GAA(x1, x2, x6)
U14_GAA(x1, x2, x3, x4, x5, x6) = U14_GAA(x1, x2, x6)
U15_GAA(x1, x2, x3, x4, x5, x6) = U15_GAA(x1, x2, x6)
U16_GAA(x1, x2, x3, x4, x5, x6) = U16_GAA(x1, x2, x4, x6)
U17_GAA(x1, x2, x3, x4, x5, x6) = U17_GAA(x1, x2, x6)
U18_GAA(x1, x2, x3, x4) = U18_GAA(x1, x4)
U19_GAA(x1, x2, x3, x4) = U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4) = U20_GAA(x1, x4)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U4_GAGAGA(x1, x3, x5, x7)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U5_GAGAGA(x1, x3, x5, x7)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DERA_IN_GA(d(e(+(t, X1))), +(const(1), X2)) → U21_GA(X1, X2, derA_in_ga(d(e(X1)), X2))
DERA_IN_GA(d(e(+(t, X1))), +(const(1), X2)) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(const(X1), X2))), +(const(0), X3)) → U22_GA(X1, X2, X3, derA_in_ga(d(e(X2)), X3))
DERA_IN_GA(d(e(+(const(X1), X2))), +(const(0), X3)) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U23_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X4, X2, X5, X3, X6))
DERA_IN_GA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → PB_IN_GAGAGA(X1, X4, X2, X5, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → U1_GAGAGA(X1, X2, X3, X4, X5, X6, derA_in_ga(d(e(X1)), X2))
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U24_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X5, X2, X4, X3, X6))
DERA_IN_GA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → PB_IN_GAGAGA(X1, X5, X2, X4, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U3_GAGAGA(X1, X2, X3, X4, X5, X6, derA_in_ga(d(e(X3)), X4))
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → DERA_IN_GA(d(e(X3)), X4)
DERA_IN_GA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U25_GA(X1, X2, derA_in_ga(d(e(X1)), X2))
DERA_IN_GA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U26_GA(X1, X2, X3, derA_in_ga(d(e(X2)), X3))
DERA_IN_GA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U27_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X5, X2, X6, X3, X4))
DERA_IN_GA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → PB_IN_GAGAGA(X1, X5, X2, X6, X3, X4)
DERA_IN_GA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U28_GA(X1, X2, X3, X4, X5, X6, pB_in_gagaga(X1, X6, X2, X5, X3, X4))
DERA_IN_GA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → PB_IN_GAGAGA(X1, X6, X2, X5, X3, X4)
DERA_IN_GA(d(d(X1)), X2) → U29_GA(X1, X2, pC_in_gaa(X1, X3, X2))
DERA_IN_GA(d(d(X1)), X2) → PC_IN_GAA(X1, X3, X2)
PC_IN_GAA(e(t), const(1), X1) → U6_GAA(X1, derA_in_ga(d(e(const(1))), X1))
PC_IN_GAA(e(t), const(1), X1) → DERA_IN_GA(d(e(const(1))), X1)
PC_IN_GAA(e(const(X1)), const(0), X2) → U7_GAA(X1, X2, derA_in_ga(d(e(const(0))), X2))
PC_IN_GAA(e(const(X1)), const(0), X2) → DERA_IN_GA(d(e(const(0))), X2)
PC_IN_GAA(e(+(X1, X2)), +(X3, X4), X5) → U8_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X1)), X3))
PC_IN_GAA(e(+(X1, X2)), +(X3, X4), X5) → DERA_IN_GA(d(e(X1)), X3)
PC_IN_GAA(e(+(X1, X2)), +(X3, X4), X5) → U9_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X3))
U9_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U10_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X2)), X4))
U9_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → DERA_IN_GA(d(e(X2)), X4)
U9_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U11_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X4))
U11_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → U12_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(+(X3, X4))), X5))
U11_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → DERA_IN_GA(d(e(+(X3, X4))), X5)
PC_IN_GAA(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U13_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X1)), X4))
PC_IN_GAA(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → DERA_IN_GA(d(e(X1)), X4)
PC_IN_GAA(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U14_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X4))
U14_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U15_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(X2)), X3))
U14_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → DERA_IN_GA(d(e(X2)), X3)
U14_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U16_GAA(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X3))
U16_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → U17_GAA(X1, X2, X3, X4, X5, derA_in_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5))
U16_GAA(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → DERA_IN_GA(d(e(+(*(X1, X3), *(X2, X4)))), X5)
PC_IN_GAA(d(X1), X2, X3) → U18_GAA(X1, X2, X3, derA_in_ga(d(X1), X4))
PC_IN_GAA(d(X1), X2, X3) → DERA_IN_GA(d(X1), X4)
PC_IN_GAA(d(X1), X2, X3) → U19_GAA(X1, X2, X3, dercA_in_ga(d(X1), X4))
U19_GAA(X1, X2, X3, dercA_out_ga(d(X1), X4)) → U20_GAA(X1, X2, X3, pC_in_gaa(e(X4), X2, X3))
U19_GAA(X1, X2, X3, dercA_out_ga(d(X1), X4)) → PC_IN_GAA(e(X4), X2, X3)
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U5_GAGAGA(X1, X2, X3, X4, X5, X6, derA_in_ga(d(e(X5)), X6))
U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → DERA_IN_GA(d(e(X5)), X6)

The TRS R consists of the following rules:

dercA_in_ga(d(e(t)), const(1)) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1))), const(0)) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1))), +(const(1), X2)) → U31_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(const(X1), X2))), +(const(0), X3)) → U32_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U33_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X4, X2, X5, X3, X6))
qcB_in_gagaga(X1, X2, X3, X4, X5, X6) → U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U34_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X4, X3, X6))
U34_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
dercA_in_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U35_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U36_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U37_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X6, X3, X4))
U37_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
dercA_in_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U38_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X6, X2, X5, X3, X4))
U38_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
dercA_in_ga(d(d(X1)), X2) → U39_ga(X1, X2, qcC_in_gaa(X1, X3, X2))
qcC_in_gaa(e(t), const(1), X1) → U43_gaa(X1, dercA_in_ga(d(e(const(1))), X1))
U43_gaa(X1, dercA_out_ga(d(e(const(1))), X1)) → qcC_out_gaa(e(t), const(1), X1)
qcC_in_gaa(e(const(X1)), const(0), X2) → U44_gaa(X1, X2, dercA_in_ga(d(e(const(0))), X2))
U44_gaa(X1, X2, dercA_out_ga(d(e(const(0))), X2)) → qcC_out_gaa(e(const(X1)), const(0), X2)
qcC_in_gaa(e(+(X1, X2)), +(X3, X4), X5) → U45_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X3))
U45_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U46_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X4))
U46_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → U47_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(X3, X4))), X5))
U47_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(X3, X4))), X5)) → qcC_out_gaa(e(+(X1, X2)), +(X3, X4), X5)
qcC_in_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U48_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X4))
U48_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U49_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X3))
U49_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → U50_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5))
U50_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5)) → qcC_out_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5)
qcC_in_gaa(d(X1), X2, X3) → U51_gaa(X1, X2, X3, dercA_in_ga(d(X1), X4))
U51_gaa(X1, X2, X3, dercA_out_ga(d(X1), X4)) → U52_gaa(X1, X2, X3, qcC_in_gaa(e(X4), X2, X3))
U52_gaa(X1, X2, X3, qcC_out_gaa(e(X4), X2, X3)) → qcC_out_gaa(d(X1), X2, X3)
U39_ga(X1, X2, qcC_out_gaa(X1, X3, X2)) → dercA_out_ga(d(d(X1)), X2)
U36_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U35_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X5)), X6))
U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)
U33_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U32_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U31_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 36 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DERA_IN_GA(d(e(+(const(X1), X2))), +(const(0), X3)) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(+(t, X1))), +(const(1), X2)) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → PB_IN_GAGAGA(X1, X4, X2, X5, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → PB_IN_GAGAGA(X1, X5, X2, X4, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → DERA_IN_GA(d(e(X3)), X4)
DERA_IN_GA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → PB_IN_GAGAGA(X1, X5, X2, X6, X3, X4)
DERA_IN_GA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → PB_IN_GAGAGA(X1, X6, X2, X5, X3, X4)
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → DERA_IN_GA(d(e(X5)), X6)

The TRS R consists of the following rules:

dercA_in_ga(d(e(t)), const(1)) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1))), const(0)) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1))), +(const(1), X2)) → U31_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(const(X1), X2))), +(const(0), X3)) → U32_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U33_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X4, X2, X5, X3, X6))
qcB_in_gagaga(X1, X2, X3, X4, X5, X6) → U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U34_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X4, X3, X6))
U34_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
dercA_in_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U35_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U36_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U37_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X6, X3, X4))
U37_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
dercA_in_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U38_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X6, X2, X5, X3, X4))
U38_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
dercA_in_ga(d(d(X1)), X2) → U39_ga(X1, X2, qcC_in_gaa(X1, X3, X2))
qcC_in_gaa(e(t), const(1), X1) → U43_gaa(X1, dercA_in_ga(d(e(const(1))), X1))
U43_gaa(X1, dercA_out_ga(d(e(const(1))), X1)) → qcC_out_gaa(e(t), const(1), X1)
qcC_in_gaa(e(const(X1)), const(0), X2) → U44_gaa(X1, X2, dercA_in_ga(d(e(const(0))), X2))
U44_gaa(X1, X2, dercA_out_ga(d(e(const(0))), X2)) → qcC_out_gaa(e(const(X1)), const(0), X2)
qcC_in_gaa(e(+(X1, X2)), +(X3, X4), X5) → U45_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X3))
U45_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U46_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X4))
U46_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → U47_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(X3, X4))), X5))
U47_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(X3, X4))), X5)) → qcC_out_gaa(e(+(X1, X2)), +(X3, X4), X5)
qcC_in_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U48_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X4))
U48_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U49_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X3))
U49_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → U50_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5))
U50_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5)) → qcC_out_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5)
qcC_in_gaa(d(X1), X2, X3) → U51_gaa(X1, X2, X3, dercA_in_ga(d(X1), X4))
U51_gaa(X1, X2, X3, dercA_out_ga(d(X1), X4)) → U52_gaa(X1, X2, X3, qcC_in_gaa(e(X4), X2, X3))
U52_gaa(X1, X2, X3, qcC_out_gaa(e(X4), X2, X3)) → qcC_out_gaa(d(X1), X2, X3)
U39_ga(X1, X2, qcC_out_gaa(X1, X3, X2)) → dercA_out_ga(d(d(X1)), X2)
U36_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U35_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X5)), X6))
U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)
U33_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U32_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U31_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))

The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
e(x1) = e(x1)
+(x1, x2) = +(x1, x2)
t = t
const(x1) = const(x1)
*(x1, x2) = *(x1, x2)
dercA_in_ga(x1, x2) = dercA_in_ga(x1)
dercA_out_ga(x1, x2) = dercA_out_ga(x1, x2)
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
U33_ga(x1, x2, x3, x4, x5, x6, x7) = U33_ga(x1, x2, x3, x7)
qcB_in_gagaga(x1, x2, x3, x4, x5, x6) = qcB_in_gagaga(x1, x3, x5)
U40_gagaga(x1, x2, x3, x4, x5, x6, x7) = U40_gagaga(x1, x3, x5, x7)
U34_ga(x1, x2, x3, x4, x5, x6, x7) = U34_ga(x1, x2, x3, x7)
qcB_out_gagaga(x1, x2, x3, x4, x5, x6) = qcB_out_gagaga(x1, x2, x3, x4, x5, x6)
U35_ga(x1, x2, x3) = U35_ga(x1, x3)
U36_ga(x1, x2, x3, x4) = U36_ga(x1, x2, x4)
U37_ga(x1, x2, x3, x4, x5, x6, x7) = U37_ga(x1, x2, x3, x7)
U38_ga(x1, x2, x3, x4, x5, x6, x7) = U38_ga(x1, x2, x3, x7)
U39_ga(x1, x2, x3) = U39_ga(x1, x3)
qcC_in_gaa(x1, x2, x3) = qcC_in_gaa(x1)
U43_gaa(x1, x2) = U43_gaa(x2)
1 = 1
qcC_out_gaa(x1, x2, x3) = qcC_out_gaa(x1, x2, x3)
U44_gaa(x1, x2, x3) = U44_gaa(x1, x3)
0 = 0
U45_gaa(x1, x2, x3, x4, x5, x6) = U45_gaa(x1, x2, x6)
U46_gaa(x1, x2, x3, x4, x5, x6) = U46_gaa(x1, x2, x3, x6)
U47_gaa(x1, x2, x3, x4, x5, x6) = U47_gaa(x1, x2, x3, x4, x6)
U48_gaa(x1, x2, x3, x4, x5, x6) = U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6) = U49_gaa(x1, x2, x4, x6)
U50_gaa(x1, x2, x3, x4, x5, x6) = U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4) = U51_gaa(x1, x4)
U52_gaa(x1, x2, x3, x4) = U52_gaa(x1, x4)
U41_gagaga(x1, x2, x3, x4, x5, x6, x7) = U41_gagaga(x1, x2, x3, x5, x7)
U42_gagaga(x1, x2, x3, x4, x5, x6, x7) = U42_gagaga(x1, x2, x3, x4, x5, x7)
DERA_IN_GA(x1, x2) = DERA_IN_GA(x1)
PB_IN_GAGAGA(x1, x2, x3, x4, x5, x6) = PB_IN_GAGAGA(x1, x3, x5)
U2_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U2_GAGAGA(x1, x3, x5, x7)
U4_GAGAGA(x1, x2, x3, x4, x5, x6, x7) = U4_GAGAGA(x1, x3, x5, x7)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DERA_IN_GA(d(e(+(const(X1), X2))), +(const(0), X3)) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(+(t, X1))), +(const(1), X2)) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → PB_IN_GAGAGA(X1, X4, X2, X5, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → PB_IN_GAGAGA(X1, X5, X2, X4, X3, X6)
PB_IN_GAGAGA(X1, X2, X3, X4, X5, X6) → U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → DERA_IN_GA(d(e(X3)), X4)
DERA_IN_GA(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → DERA_IN_GA(d(e(X1)), X2)
DERA_IN_GA(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → DERA_IN_GA(d(e(X2)), X3)
DERA_IN_GA(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → PB_IN_GAGAGA(X1, X5, X2, X6, X3, X4)
DERA_IN_GA(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → PB_IN_GAGAGA(X1, X6, X2, X5, X3, X4)
U2_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U4_GAGAGA(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → DERA_IN_GA(d(e(X5)), X6)

The TRS R consists of the following rules:

dercA_in_ga(d(e(t)), const(1)) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1))), const(0)) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1))), +(const(1), X2)) → U31_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(const(X1), X2))), +(const(0), X3)) → U32_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U33_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X4, X2, X5, X3, X6))
dercA_in_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U34_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X4, X3, X6))
dercA_in_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U35_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U36_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U37_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X6, X3, X4))
dercA_in_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U38_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X6, X2, X5, X3, X4))
U31_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))
U32_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U33_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U34_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
U35_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U36_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U37_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
U38_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
qcB_in_gagaga(X1, X2, X3, X4, X5, X6) → U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X5)), X6))
U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DERA_IN_GA(d(e(+(const(X1), X2)))) → DERA_IN_GA(d(e(X2)))
DERA_IN_GA(d(e(+(t, X1)))) → DERA_IN_GA(d(e(X1)))
DERA_IN_GA(d(e(+(+(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
PB_IN_GAGAGA(X1, X3, X5) → DERA_IN_GA(d(e(X1)))
DERA_IN_GA(d(e(+(*(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
PB_IN_GAGAGA(X1, X3, X5) → U2_GAGAGA(X1, X3, X5, dercA_in_ga(d(e(X1))))
U2_GAGAGA(X1, X3, X5, dercA_out_ga(d(e(X1)), X2)) → DERA_IN_GA(d(e(X3)))
DERA_IN_GA(d(e(*(t, X1)))) → DERA_IN_GA(d(e(X1)))
DERA_IN_GA(d(e(*(const(X1), X2)))) → DERA_IN_GA(d(e(X2)))
DERA_IN_GA(d(e(*(+(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
DERA_IN_GA(d(e(*(*(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
U2_GAGAGA(X1, X3, X5, dercA_out_ga(d(e(X1)), X2)) → U4_GAGAGA(X1, X3, X5, dercA_in_ga(d(e(X3))))
U4_GAGAGA(X1, X3, X5, dercA_out_ga(d(e(X3)), X4)) → DERA_IN_GA(d(e(X5)))

The TRS R consists of the following rules:

dercA_in_ga(d(e(t))) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1)))) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1)))) → U31_ga(X1, dercA_in_ga(d(e(X1))))
dercA_in_ga(d(e(+(const(X1), X2)))) → U32_ga(X1, X2, dercA_in_ga(d(e(X2))))
dercA_in_ga(d(e(+(+(X1, X2), X3)))) → U33_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
dercA_in_ga(d(e(+(*(X1, X2), X3)))) → U34_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
dercA_in_ga(d(e(*(t, X1)))) → U35_ga(X1, dercA_in_ga(d(e(X1))))
dercA_in_ga(d(e(*(const(X1), X2)))) → U36_ga(X1, X2, dercA_in_ga(d(e(X2))))
dercA_in_ga(d(e(*(+(X1, X2), X3)))) → U37_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
dercA_in_ga(d(e(*(*(X1, X2), X3)))) → U38_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
U31_ga(X1, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))
U32_ga(X1, X2, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U33_ga(X1, X2, X3, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U34_ga(X1, X2, X3, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
U35_ga(X1, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U36_ga(X1, X2, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U37_ga(X1, X2, X3, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
U38_ga(X1, X2, X3, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
qcB_in_gagaga(X1, X3, X5) → U40_gagaga(X1, X3, X5, dercA_in_ga(d(e(X1))))
U40_gagaga(X1, X3, X5, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X5, dercA_in_ga(d(e(X3))))
U41_gagaga(X1, X2, X3, X5, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X5))))
U42_gagaga(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)

The set Q consists of the following terms:

dercA_in_ga(x0)
U31_ga(x0, x1)
U32_ga(x0, x1, x2)
U33_ga(x0, x1, x2, x3)
U34_ga(x0, x1, x2, x3)
U35_ga(x0, x1)
U36_ga(x0, x1, x2)
U37_ga(x0, x1, x2, x3)
U38_ga(x0, x1, x2, x3)
qcB_in_gagaga(x0, x1, x2)
U40_gagaga(x0, x1, x2, x3)
U41_gagaga(x0, x1, x2, x3, x4)
U42_gagaga(x0, x1, x2, x3, x4, x5)

We have to consider all (P,Q,R)-chains.

(12) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

DERA_IN_GA(d(e(+(const(X1), X2)))) → DERA_IN_GA(d(e(X2)))
DERA_IN_GA(d(e(+(t, X1)))) → DERA_IN_GA(d(e(X1)))
DERA_IN_GA(d(e(+(+(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
PB_IN_GAGAGA(X1, X3, X5) → DERA_IN_GA(d(e(X1)))
DERA_IN_GA(d(e(+(*(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
U2_GAGAGA(X1, X3, X5, dercA_out_ga(d(e(X1)), X2)) → DERA_IN_GA(d(e(X3)))
DERA_IN_GA(d(e(*(t, X1)))) → DERA_IN_GA(d(e(X1)))
DERA_IN_GA(d(e(*(const(X1), X2)))) → DERA_IN_GA(d(e(X2)))
DERA_IN_GA(d(e(*(+(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
DERA_IN_GA(d(e(*(*(X1, X2), X3)))) → PB_IN_GAGAGA(X1, X2, X3)
U4_GAGAGA(X1, X3, X5, dercA_out_ga(d(e(X3)), X4)) → DERA_IN_GA(d(e(X5)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(*(x₁, x₂)) = 1 + x₁ + x₂
POL(+(x₁, x₂)) = 1 + x₁ + x₂
POL(0) = 0
POL(1) = 0
POL(DERA_IN_GA(x₁)) = x₁
POL(PB_IN_GAGAGA(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U2_GAGAGA(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃
POL(U31_ga(x₁, x₂)) = 0
POL(U32_ga(x₁, x₂, x₃)) = 0
POL(U33_ga(x₁, x₂, x₃, x₄)) = 0
POL(U34_ga(x₁, x₂, x₃, x₄)) = 0
POL(U35_ga(x₁, x₂)) = 0
POL(U36_ga(x₁, x₂, x₃)) = 0
POL(U37_ga(x₁, x₂, x₃, x₄)) = 0
POL(U38_ga(x₁, x₂, x₃, x₄)) = 0
POL(U40_gagaga(x₁, x₂, x₃, x₄)) = 0
POL(U41_gagaga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U42_gagaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(U4_GAGAGA(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(const(x₁)) = 0
POL(d(x₁)) = x₁
POL(dercA_in_ga(x₁)) = 0
POL(dercA_out_ga(x₁, x₂)) = 0
POL(e(x₁)) = x₁
POL(qcB_in_gagaga(x₁, x₂, x₃)) = 0
POL(qcB_out_gagaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(t) = 1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PB_IN_GAGAGA(X1, X3, X5) → U2_GAGAGA(X1, X3, X5, dercA_in_ga(d(e(X1))))
U2_GAGAGA(X1, X3, X5, dercA_out_ga(d(e(X1)), X2)) → U4_GAGAGA(X1, X3, X5, dercA_in_ga(d(e(X3))))

The TRS R consists of the following rules:

dercA_in_ga(d(e(t))) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1)))) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1)))) → U31_ga(X1, dercA_in_ga(d(e(X1))))
dercA_in_ga(d(e(+(const(X1), X2)))) → U32_ga(X1, X2, dercA_in_ga(d(e(X2))))
dercA_in_ga(d(e(+(+(X1, X2), X3)))) → U33_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
dercA_in_ga(d(e(+(*(X1, X2), X3)))) → U34_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
dercA_in_ga(d(e(*(t, X1)))) → U35_ga(X1, dercA_in_ga(d(e(X1))))
dercA_in_ga(d(e(*(const(X1), X2)))) → U36_ga(X1, X2, dercA_in_ga(d(e(X2))))
dercA_in_ga(d(e(*(+(X1, X2), X3)))) → U37_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
dercA_in_ga(d(e(*(*(X1, X2), X3)))) → U38_ga(X1, X2, X3, qcB_in_gagaga(X1, X2, X3))
U31_ga(X1, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))
U32_ga(X1, X2, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U33_ga(X1, X2, X3, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U34_ga(X1, X2, X3, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
U35_ga(X1, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U36_ga(X1, X2, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U37_ga(X1, X2, X3, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
U38_ga(X1, X2, X3, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
qcB_in_gagaga(X1, X3, X5) → U40_gagaga(X1, X3, X5, dercA_in_ga(d(e(X1))))
U40_gagaga(X1, X3, X5, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X5, dercA_in_ga(d(e(X3))))
U41_gagaga(X1, X2, X3, X5, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X5))))
U42_gagaga(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)

The set Q consists of the following terms:

dercA_in_ga(x0)
U31_ga(x0, x1)
U32_ga(x0, x1, x2)
U33_ga(x0, x1, x2, x3)
U34_ga(x0, x1, x2, x3)
U35_ga(x0, x1)
U36_ga(x0, x1, x2)
U37_ga(x0, x1, x2, x3)
U38_ga(x0, x1, x2, x3)
qcB_in_gagaga(x0, x1, x2)
U40_gagaga(x0, x1, x2, x3)
U41_gagaga(x0, x1, x2, x3, x4)
U42_gagaga(x0, x1, x2, x3, x4, x5)

We have to consider all (P,Q,R)-chains.

(14) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(15) TRUE

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GAA(d(X1), X2, X3) → DERA_IN_GA(d(X1), X4)
DERA_IN_GA(d(d(X1)), X2) → PC_IN_GAA(X1, X3, X2)

The TRS R consists of the following rules:

dercA_in_ga(d(e(t)), const(1)) → dercA_out_ga(d(e(t)), const(1))
dercA_in_ga(d(e(const(X1))), const(0)) → dercA_out_ga(d(e(const(X1))), const(0))
dercA_in_ga(d(e(+(t, X1))), +(const(1), X2)) → U31_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(const(X1), X2))), +(const(0), X3)) → U32_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6)) → U33_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X4, X2, X5, X3, X6))
qcB_in_gagaga(X1, X2, X3, X4, X5, X6) → U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6)) → U34_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X4, X3, X6))
U34_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X4, X3, X6)) → dercA_out_ga(d(e(+(*(X1, X2), X3))), +(+(*(X1, X4), *(X2, X5)), X6))
dercA_in_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1)))) → U35_ga(X1, X2, dercA_in_ga(d(e(X1)), X2))
dercA_in_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0)))) → U36_ga(X1, X2, X3, dercA_in_ga(d(e(X2)), X3))
dercA_in_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6)))) → U37_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X5, X2, X6, X3, X4))
U37_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X5, X2, X6, X3, X4)) → dercA_out_ga(d(e(*(+(X1, X2), X3))), +(*(+(X1, X2), X4), *(X3, +(X5, X6))))
dercA_in_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6))))) → U38_ga(X1, X2, X3, X4, X5, X6, qcB_in_gagaga(X1, X6, X2, X5, X3, X4))
U38_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X6, X2, X5, X3, X4)) → dercA_out_ga(d(e(*(*(X1, X2), X3))), +(*(*(X1, X2), X4), *(X3, +(*(X1, X5), *(X2, X6)))))
dercA_in_ga(d(d(X1)), X2) → U39_ga(X1, X2, qcC_in_gaa(X1, X3, X2))
qcC_in_gaa(e(t), const(1), X1) → U43_gaa(X1, dercA_in_ga(d(e(const(1))), X1))
U43_gaa(X1, dercA_out_ga(d(e(const(1))), X1)) → qcC_out_gaa(e(t), const(1), X1)
qcC_in_gaa(e(const(X1)), const(0), X2) → U44_gaa(X1, X2, dercA_in_ga(d(e(const(0))), X2))
U44_gaa(X1, X2, dercA_out_ga(d(e(const(0))), X2)) → qcC_out_gaa(e(const(X1)), const(0), X2)
qcC_in_gaa(e(+(X1, X2)), +(X3, X4), X5) → U45_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X3))
U45_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X3)) → U46_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X4))
U46_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X4)) → U47_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(X3, X4))), X5))
U47_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(X3, X4))), X5)) → qcC_out_gaa(e(+(X1, X2)), +(X3, X4), X5)
qcC_in_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5) → U48_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X1)), X4))
U48_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X1)), X4)) → U49_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(X2)), X3))
U49_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(X2)), X3)) → U50_gaa(X1, X2, X3, X4, X5, dercA_in_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5))
U50_gaa(X1, X2, X3, X4, X5, dercA_out_ga(d(e(+(*(X1, X3), *(X2, X4)))), X5)) → qcC_out_gaa(e(*(X1, X2)), +(*(X1, X3), *(X2, X4)), X5)
qcC_in_gaa(d(X1), X2, X3) → U51_gaa(X1, X2, X3, dercA_in_ga(d(X1), X4))
U51_gaa(X1, X2, X3, dercA_out_ga(d(X1), X4)) → U52_gaa(X1, X2, X3, qcC_in_gaa(e(X4), X2, X3))
U52_gaa(X1, X2, X3, qcC_out_gaa(e(X4), X2, X3)) → qcC_out_gaa(d(X1), X2, X3)
U39_ga(X1, X2, qcC_out_gaa(X1, X3, X2)) → dercA_out_ga(d(d(X1)), X2)
U36_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(*(const(X1), X2))), +(*(const(X1), X3), *(X2, const(0))))
U35_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(*(t, X1))), +(*(t, X2), *(X1, const(1))))
U40_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X1)), X2)) → U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X3)), X4))
U41_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X3)), X4)) → U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_in_ga(d(e(X5)), X6))
U42_gagaga(X1, X2, X3, X4, X5, X6, dercA_out_ga(d(e(X5)), X6)) → qcB_out_gagaga(X1, X2, X3, X4, X5, X6)
U33_ga(X1, X2, X3, X4, X5, X6, qcB_out_gagaga(X1, X4, X2, X5, X3, X6)) → dercA_out_ga(d(e(+(+(X1, X2), X3))), +(+(X4, X5), X6))
U32_ga(X1, X2, X3, dercA_out_ga(d(e(X2)), X3)) → dercA_out_ga(d(e(+(const(X1), X2))), +(const(0), X3))
U31_ga(X1, X2, dercA_out_ga(d(e(X1)), X2)) → dercA_out_ga(d(e(+(t, X1))), +(const(1), X2))

The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
e(x1) = e(x1)
+(x1, x2) = +(x1, x2)
t = t
const(x1) = const(x1)
*(x1, x2) = *(x1, x2)
dercA_in_ga(x1, x2) = dercA_in_ga(x1)
dercA_out_ga(x1, x2) = dercA_out_ga(x1, x2)
U31_ga(x1, x2, x3) = U31_ga(x1, x3)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
U33_ga(x1, x2, x3, x4, x5, x6, x7) = U33_ga(x1, x2, x3, x7)
qcB_in_gagaga(x1, x2, x3, x4, x5, x6) = qcB_in_gagaga(x1, x3, x5)
U40_gagaga(x1, x2, x3, x4, x5, x6, x7) = U40_gagaga(x1, x3, x5, x7)
U34_ga(x1, x2, x3, x4, x5, x6, x7) = U34_ga(x1, x2, x3, x7)
qcB_out_gagaga(x1, x2, x3, x4, x5, x6) = qcB_out_gagaga(x1, x2, x3, x4, x5, x6)
U35_ga(x1, x2, x3) = U35_ga(x1, x3)
U36_ga(x1, x2, x3, x4) = U36_ga(x1, x2, x4)
U37_ga(x1, x2, x3, x4, x5, x6, x7) = U37_ga(x1, x2, x3, x7)
U38_ga(x1, x2, x3, x4, x5, x6, x7) = U38_ga(x1, x2, x3, x7)
U39_ga(x1, x2, x3) = U39_ga(x1, x3)
qcC_in_gaa(x1, x2, x3) = qcC_in_gaa(x1)
U43_gaa(x1, x2) = U43_gaa(x2)
1 = 1
qcC_out_gaa(x1, x2, x3) = qcC_out_gaa(x1, x2, x3)
U44_gaa(x1, x2, x3) = U44_gaa(x1, x3)
0 = 0
U45_gaa(x1, x2, x3, x4, x5, x6) = U45_gaa(x1, x2, x6)
U46_gaa(x1, x2, x3, x4, x5, x6) = U46_gaa(x1, x2, x3, x6)
U47_gaa(x1, x2, x3, x4, x5, x6) = U47_gaa(x1, x2, x3, x4, x6)
U48_gaa(x1, x2, x3, x4, x5, x6) = U48_gaa(x1, x2, x6)
U49_gaa(x1, x2, x3, x4, x5, x6) = U49_gaa(x1, x2, x4, x6)
U50_gaa(x1, x2, x3, x4, x5, x6) = U50_gaa(x1, x2, x3, x4, x6)
U51_gaa(x1, x2, x3, x4) = U51_gaa(x1, x4)
U52_gaa(x1, x2, x3, x4) = U52_gaa(x1, x4)
U41_gagaga(x1, x2, x3, x4, x5, x6, x7) = U41_gagaga(x1, x2, x3, x5, x7)
U42_gagaga(x1, x2, x3, x4, x5, x6, x7) = U42_gagaga(x1, x2, x3, x4, x5, x7)
DERA_IN_GA(x1, x2) = DERA_IN_GA(x1)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PC_IN_GAA(d(X1), X2, X3) → DERA_IN_GA(d(X1), X4)
DERA_IN_GA(d(d(X1)), X2) → PC_IN_GAA(X1, X3, X2)

R is empty.
The argument filtering Pi contains the following mapping:
d(x1) = d(x1)
DERA_IN_GA(x1, x2) = DERA_IN_GA(x1)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PC_IN_GAA(d(X1)) → DERA_IN_GA(d(X1))
DERA_IN_GA(d(d(X1))) → PC_IN_GAA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DERA_IN_GA(d(d(X1))) → PC_IN_GAA(X1)
The graph contains the following edges 1 > 1
PC_IN_GAA(d(X1)) → DERA_IN_GA(d(X1))
The graph contains the following edges 1 >= 1

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPOrderProof (EQUIVALENT transformation)

(13) Obligation:

(14) DependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES